// ***** This file is automatically generated from Bound.java.jpp

package daikon.inv.unary.scalar;

import daikon.*;
import daikon.inv.*;

  import daikon.inv.unary.sequence.*;
  import daikon.inv.binary.sequenceScalar.*;

import daikon.inv.unary.*;
import daikon.derive.unary.*;
import plume.*;

import java.util.*;

  /**
   * Represents the invariant <samp>x <= c</samp>, where <samp>c</samp>
   * is a constant and <samp>x</samp> is a long scalar.
   **/

// One reason not to combine LowerBound and UpperBound into a single range
// invariant is that they have separate justifications:  one may be
// justified when the other is not.
public class UpperBound
  extends SingleScalar
{
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20030822L;

  // Variables starting with dkconfig_ should only be set via the
  // daikon.config.Configuration interface.
  /**
   * Boolean.  True iff UpperBound invariants should be considered.
   **/
  public static boolean dkconfig_enabled = true;
  /**
   * Long integer.  Together with the corresponding
   * <code>maximal_interesting</code> parameter, specifies the
   * range of the computed constant that is ``interesting'' --- the range
   * that should be reported.  For instance, setting
   * <code>minimal_interesting</code>
   * to -1 and <code>maximal_interesting</code>
   * to 2 would only permit output of
   * UpperBound invariants whose cutoff was one of (-1,0,1,2).
   **/
  public static long dkconfig_minimal_interesting = -1;
  /**
   * Long integer.  Together with the corresponding
   * <code>minimal_interesting</code> parameter, specifies the
   * range of the computed constant that is ``interesting'' --- the range
   * that should be reported.  For instance, setting
   * <code>minimal_interesting</code>
   * to -1 and <code>maximal_interesting</code>
   * to 2 would only permit output of
   * UpperBound invariants whose cutoff was one of (-1,0,1,2).
   **/
  public static long dkconfig_maximal_interesting = 2;

  private UpperBoundCore core;

  @SuppressWarnings("nullness") // circular initialization
  private UpperBound(PptSlice slice) {
    super (slice);
    assert slice != null;
    core = new UpperBoundCore(this);
  }

  private /*@Prototype*/ UpperBound() {
    super ();
    // do we need a core?
  }

  private static /*@Prototype*/ UpperBound proto;

  /** Returns the prototype invariant for UpperBound **/
  public static /*@Prototype*/ UpperBound get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ UpperBound ();
    return (proto);
  }

  /** returns whether or not this invariant is enabled **/
  public boolean enabled() {
    return dkconfig_enabled;
  }

  /** UpperBound is only valid on integral types **/
  public boolean instantiate_ok (VarInfo[] vis) {

    if (!valid_types (vis))
      return (false);

    return (vis[0].file_rep_type.baseIsIntegral());
    }

  /** instantiate an invariant on the specified slice **/
  public UpperBound instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new UpperBound (slice);
  }

  public UpperBound clone() {
    UpperBound result = (UpperBound) super.clone();
    result.core = core.clone();
    result.core.wrapper = result;
    return result;
  }

  public long max() {
    return core.max();          // i.e., core.max1
  }

  public String repr() {
    return "UpperBound" + varNames() + ": "
      + core.repr();
  }

  public String format_using(OutputFormat format) {
    String name = var().name_using(format);
    PptTopLevel pptt = ppt.parent;

    if ((format == OutputFormat.DAIKON)
        || (format == OutputFormat.ESCJAVA)
        || (format.isJavaFamily()))
    {

      if (PrintInvariants.dkconfig_static_const_infer) {
        for (VarInfo vi : pptt.var_infos) {
          // Check is static constant, and variables are comparable
          if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
            // If variable is a double, then use fuzzy comparison
            if (vi.rep_type == ProglangType.DOUBLE) {
              Double constantVal = (Double)vi.constantValue();
              if (Global.fuzzy.eq(constantVal, core.max1) || (Double.isNaN(constantVal) && Double.isNaN(core.max1)))
                return name + " <= " + vi.name();
            }
            // Otherwise just use the equals method
            else {
              Object constantVal = vi.constantValue();
              if (constantVal.equals(core.max1)) {
                return name + " <= " + vi.name();
              }
            }
          }
        }
      }

      return name + " <= " + core.max1;
    }

    if (format == OutputFormat.SIMPLIFY) {

      return "(<= " + name + " " + simplify_format_long(core.max1) + ")";
    }

    return format_unimplemented(format);
  }

  public InvariantStatus add_modified(long value, int count) {
    // System.out.println("UpperBound" + varNames() + ": "
    //              + "add(" + value + ", " + modified + ", " + count + ")");

    return core.add_modified(value, count);

  }

  public InvariantStatus check_modified(long value, int count) {

    return core.check(value);

  }

  public boolean enoughSamples() {
    return core.enoughSamples();
  }

  protected double computeConfidence() {
    return core.computeConfidence();
  }

  public boolean isExact() {
    return core.isExact();
  }

  public boolean isSameFormula(Invariant other) {
    return core.isSameFormula(((UpperBound) other).core);
  }

  // XXX FIXME This looks like a hack that should be removed.  -MDE 6/13/2002
  // Use hasUninterestingConstant() instead. -SMcC 2/26/2003
  public boolean isInteresting() {
    return (-1 < core.max1 && core.max1 < 2);
  }

  public boolean hasUninterestingConstant() {
    // If the constant bound is not in some small range of interesting
    // values (by default {-1, 0, 1, 2}), call it uninteresting.
    if ((core.max1 < dkconfig_minimal_interesting) ||
        (core.max1 > dkconfig_maximal_interesting)) {
      return true;
    }

    return false;
  }

  public /*@Nullable*/ DiscardInfo isObviousStatically (VarInfo[] vis) {
    VarInfo var = vis[0];
    if ((var.derived instanceof SequenceLength)
         && (((SequenceLength) var.derived).shift != 0)) {
      return new DiscardInfo(this, DiscardCode.obvious, "Bounds are preferrable over"
                             + " sequence lengths with no shift");
    }
    return super.isObviousStatically (vis);
  }

  public /*@Nullable*/ DiscardInfo isObviousDynamically(VarInfo[] vis) {
    DiscardInfo super_result = super.isObviousDynamically(vis);
    if (super_result != null) {
      return super_result;
    }

    PptTopLevel pptt = ppt.parent;

    // This check always lets invariants pass through (even if it is not within
    // the default range of (-1 to 2) if it matches a static constant
    // As noted below, this check really doesn't belong here, but should be
    // moved to hasUninterestingConstant() whenever that is implemented
    if (PrintInvariants.dkconfig_static_const_infer) {
      if (core.matchConstant()) {
        return null;
      }
    }

    // if the value is not in some range (like -1,0,1,2) then say that it is obvious
    if ((core.max1 < dkconfig_minimal_interesting) ||
        (core.max1 > dkconfig_maximal_interesting)) {
      // XXX This check doesn't really belong here. However It
      // shouldn't get removed until hasUninterestingConstant() is
      // suitable to be turned on everywhere by default. -SMcC
      // if the value is not in some range (like -1,0,1,2) then say that
      // it is obvious
      String discardString = "";
      if (core.max1 < dkconfig_minimal_interesting) {
        discardString = "MIN1="+core.max1+" is less than dkconfig_minimal_interesting=="
          + dkconfig_minimal_interesting;
      } else {
        discardString = "MIN1="+core.max1+" is greater than dkconfig_maximal_interesting=="+
          dkconfig_maximal_interesting;
      }
      return new DiscardInfo(this, DiscardCode.obvious, discardString);
    }
    OneOfScalar oo = OneOfScalar.find(ppt);
    if ((oo != null) && oo.enoughSamples() && oo.num_elts() > 0) {
      assert oo.var().isCanonical();
      // We could also use core.max1 == oo.max_elt(), since the LowerBound
      // will never have a core.max1 that does not appear in the OneOf.
      if (core.max1 >= oo.max_elt()) {
        String varName = vis[0].name();
        String discardString = varName+">="+core.max1+" is implied by "+varName+">="+oo.max_elt();
        log (discardString);
        return new DiscardInfo(this, DiscardCode.obvious, discardString);
      }
    }

    // NOT: "VarInfo v = var();" because we want to operate not on this
    // object's own variables, but on the variables that were passed in.
    VarInfo v = vis[0];

    // For each sequence variable, if this is an obvious member/subsequence, and
    // it has the same invariant, then this one is obvious.
    for (int i=0; i<pptt.var_infos.length; i++) {
      VarInfo vi = pptt.var_infos[i];

      if (Member.isObviousMember(v, vi))
      {
        PptSlice1 other_slice = pptt.findSlice(vi);
        if (other_slice != null) {
          EltUpperBound eb = EltUpperBound.find(other_slice);
          if ((eb != null)
              && eb.enoughSamples()
              && eb.max() == max()) {
            String otherName = other_slice.var_infos[0].name();
            String varName = v.name();
            String discardString = varName+" is a subsequence of "+otherName+" for which the invariant holds.";
            log (discardString);
            return new DiscardInfo(this, DiscardCode.obvious, discardString);
          }
        }
      }
    }

    return null;
  }

  public boolean isExclusiveFormula(Invariant other) {

    if (other instanceof LowerBound) {
      if (max() < ((LowerBound) other).min())
        return true;
    }

    if (other instanceof OneOfScalar) {
      return other.isExclusiveFormula(this);
    }
    return false;
  }

  // Look up a previously instantiated invariant.
  public static /*@Nullable*/ UpperBound find(PptSlice ppt) {
    assert ppt.arity() == 1;
    for (Invariant inv : ppt.invs) {
      if (inv instanceof UpperBound)
        return (UpperBound) inv;
    }
    return null;
  }

  /**
   * Bound can merge different formulas from lower points to create a single
   * formula at an upper point.  See merge() below.
   */
  public boolean mergeFormulasOk() {
    return (true);
  }

  /**
   * Merge the invariants in invs to form a new invariant.  Each must be
   * a UpperBound invariant.  This code finds all of the min/max values
   * in each invariant, applies them to a new parent invariant and
   * returns the merged invariant (if any).
   *
   * @param invs        List of invariants to merge.  The invariants must all
   *                    be of the same type and should come from the
   *                    children of parent_ppt.  They should also all
   *                    be permuted to match the variable order in
   *                    parent_ppt.
   * @param parent_ppt  Slice that will contain the new invariant
   */
  public /*@Nullable*/ Invariant merge (List<Invariant> invs, PptSlice parent_ppt) {

    // Create the initial parent invariant from the first child
    UpperBound first = (UpperBound) invs.get(0);
    UpperBound result= first.clone();
    result.ppt = parent_ppt;

    // Loop through the rest of the child invariants
    for (int i = 1; i < invs.size(); i++ ) {
      UpperBound lb = (UpperBound) invs.get (i);
      result.core.add(lb.core);
    }

    result.log ("Merged '" + result.format() + "' from " + invs.size()
                + " child invariants");
    return (result);
  }
}
